(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(x1) → x1
a(b(x1)) → b(a(c(a(a(x1)))))
c(c(c(x1))) → b(x1)

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3.
The certificate found is represented by the following graph.
Start state: 301
Accept states: [302, 303]
Transitions:
301→302[a_1|0]
301→303[c_1|0]
301→301[b_1|0]
301→304[a_1|1]
301→305[a_1|2]
301→306[c_1|2]
304→305[a_1|1]
304→306[c_1|2]
305→306[c_1|1]
306→307[a_1|1]
306→302[b_1|2]
306→304[b_1|2]
306→305[b_1|2]
306→308[a_1|2]
306→309[a_1|2, a_1|3]
306→310[c_1|3, c_1|2]
307→302[b_1|1]
307→304[b_1|1]
307→305[b_1|1]
307→308[a_1|2]
307→309[a_1|3]
307→310[c_1|3]
308→309[a_1|2]
308→310[c_1|3]
309→310[c_1|2]
310→311[a_1|2]
310→305[b_1|3]
311→305[b_1|2]

(2) BOUNDS(O(1), O(n^1))